#include<stdio.h>

int main(){
	char s[7] = "97531", c;
	char *a = s;
	c = getchar();
	while(*(a++)!='\0');
	while(*(a-1)<c){
		*(a--) = *(a-1);
	}
	*(a--) = c;
	puts(s);
	return 0;
}
